$\forall$$T$:Type, $L$:$T$ List, $P$:($\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$$\rightarrow$Prop).
\\[0ex]($\forall$$x$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$. Dec($P$($x$)))
\\[0ex]$\Rightarrow$ ($\exists$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$. $P$($i$))
\\[0ex]$\Rightarrow$ ($\exists$$i$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$. $P$($i$) \& ($\forall$$j$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L$$\parallel$}}$. $i$$<$$j$ $\Rightarrow$ $\neg$$P$($j$)))